(declare-fun a () 
